Move Doc/tools/sphinxext content to Doc/tools, there is no need for the nested subdirectory anymore.
diff --git a/Doc/Makefile b/Doc/Makefile index fee7fc7..5b5f68a 100644 --- a/Doc/Makefile +++ b/Doc/Makefile
@@ -8,7 +8,7 @@ SPHINXBUILD = sphinx-build PAPER = SOURCES = -DISTVERSION = $(shell $(PYTHON) tools/sphinxext/patchlevel.py) +DISTVERSION = $(shell $(PYTHON) tools/patchlevel.py) ALLSPHINXOPTS = -b $(BUILDER) -d build/doctrees -D latex_paper_size=$(PAPER) \ $(SPHINXOPTS) . build/$(BUILDER) $(SOURCES) @@ -79,7 +79,7 @@ @$(MAKE) build BUILDER=$(BUILDER) || { \ echo "Suspicious check complete; look for any errors in the above output" \ "or in build/$(BUILDER)/suspicious.csv. If all issues are false" \ - "positives, append that file to tools/sphinxext/susp-ignored.csv."; \ + "positives, append that file to tools/susp-ignored.csv."; \ false; } coverage: BUILDER = coverage 